T:Type, L:T List, R:({x:T| (x  L) }Realizer), es:ES.
Consistent(xL.R(x);es)  (xL. Consistent(R(x);es)) 

latex

Definitions	x:A. B(x), t  T, P  Q, Consistent(R;es), xL.R(x), x(s), xL. P(x), (L), map(f;as), P  Q, Y, reduce(f;k;as), P & Q, P  Q, Prop, True, A & B, l[i], {i..j}, ||as||, i  j < k, hd(l), nth_tl(n;as), if b t else f fi, ij, b, i<j, true, false, x. t(x), P  Q, {T}, False
Lemmas	l member wf, R-consistent wf, Rnone wf, event system wf, es realizer wf, nil member, iff functionality wrt iff, select member, length wf1, non neg length, Rall wf, cons member, and functionality wrt iff